Nuprl Lemma : decidable__dset_eq 13,42

s:DSet, a, b:|s|. Dec(a = b) 
latex


Upsets 1
Definitions of StatementDSet
DefinitionsP & Q, t  T, , P  Q, x f y, P  Q, x:A. B(x), P  Q, DSet
Lemmasdset wf, set car wf, decidable assert, assert of dset eq, set eq wf, assert wf, decidable functionality

origin